Step of Proof: p-fun-exp-add-sq
11,40
postcript
pdf
Inference at
*
2
2
1
2
1
I
of proof for Lemma
p-fun-exp-add-sq
:
.....truecase..... NILNIL
1.
A
: Type
2.
f
:
A
(
A
+ Top)
3.
x
:
A
4.
m
:
5. 0 <
m
6.
n
:
. (
can-apply(
f
^
m
- 1;
x
))
((
f
^
n
+(
m
- 1)(
x
)) ~ (
f
^
n
(do-apply(
f
^
m
- 1;
x
))))
7.
n
:
8.
can-apply(
f
^
m
;
x
)
9.
(
n
= 0)
10.
(
n
+
m
= 0)
11.
(
n
= 0)
12.
(
m
= 0)
13.
can-apply(
f
^
m
- 1;
x
)
(
f
o
f
^
n
(do-apply(
f
^
m
- 1;
x
))) ~ (
f
o
f
^
n
- 1 (outl(
f
(do-apply(
f
^
m
- 1;
x
)))))
latex
by ((GenConclAtAddr [1;2])
CollapseTHENA (Auto
)
)
CollapseTHEN (RenameVar `x1' (-2))
latex
C
1
:
C1:
14.
x1
:
A
C1:
15. do-apply(
f
^
m
- 1;
x
) =
x1
C1:
(
f
o
f
^
n
(
x1
)) ~ (
f
o
f
^
n
- 1 (outl(
f
(
x1
))))
C
.
Definitions
do-apply(
f
;
x
)
,
f
^
n
,
s
=
t
,
x
:
A
.
B
(
x
)
,
P
Q
,
x
:
A
B
(
x
)
,
t
T
origin